﻿using System;
using System.Text;
using System.Collections.Generic;
using System.Linq;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using Microsoft.Pex.Framework;


namespace Benchmarks.McMinnThesisBen
{
    [TestClass]
    public class Stack
    {
        static int MAX_ELEMENTS = 3;
        static int NO_ERROR = 0;
        static int STACK_UNDERFLOW = 1;
        static int STACK_OVERFLOW = 2;

        int[] elements;
        int size;
        int error;

        public Stack()
        {
            elements = new int[MAX_ELEMENTS];
            size = 0;
            error = 0;        
        }

        public int pop()
        {
            error = NO_ERROR;
            if (size <= 0)
            {
                error = STACK_UNDERFLOW;
            }
            if (error == NO_ERROR)
            {
                size--;
                return elements[size];
            }
            else
            {
                return 0;
            }
        }

        public void push(int element)
        {
            error = NO_ERROR;
            if (size >= MAX_ELEMENTS) //Original code is if (size > MAX_ELEMENTS)
            {
                error = STACK_OVERFLOW;
            }
            if (error == NO_ERROR)
            {
                elements[size] = element;
                size++;
            }
        }

        public int check_error()
        {
            return error;
        }

        public int check_size()
        {
            return size;
        }

        public void reset()
        {
            size = 0;
            error = 0;
        }

        //run with C:\pex\bin\Debug>Pex Benchmarks.dll /mf:TestStackFitness
        // adding /fte outputs all generated tests
        //[PexMethod(MaxRuns = 100, MaxConditions = int.MaxValue, MaxRunsWithoutNewTests = int.MaxValue)]        
        //public void TestStackFitness(
        //                    int[] modifiers, int[] elements)
        //{
        //    TestStack(modifiers, elements);
        //}

        //run with C:\pex\bin\Debug>Pex Benchmarks.dll /mf:TestStackDefault
        // adding /fte outputs all generated tests
        //[PexMethod(MaxRuns = 100, MaxConditions = int.MaxValue, MaxRunsWithoutNewTests = int.MaxValue)]
        //public void TestStackDefault(
        //                    int[] modifiers, int[] elements)
        //{
        //    TestStack(modifiers, elements);
        //}

        //private void TestStack(
        //                    int[] modifiers, int[] elements)
        //{
        //    PexAssume.IsTrue(modifiers != null);
        //    PexAssume.IsTrue(elements != null);
        //    PexAssume.IsTrue(modifiers.Length == elements.Length);

        //    Stack c = new Stack();
        //    for (int i = 0; i <= (modifiers.Length - 1); i++)
        //    {
        //        switch (modifiers[i])
        //        {
        //            case 0:
        //                c.push(elements[i]);
        //                break;
        //            case 1:
        //                c.pop();
        //                break;
        //            default:
        //                c.reset();
        //                break;
        //        }
        //    }
        //    c.check_error();
        //    c.check_size();
        //}
    }
}
